0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 24 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 54 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 9 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 2 ms)
↳27 QDP
↳28 MRRProof (⇔, 38 ms)
↳29 QDP
↳30 PisEmptyProof (⇔, 0 ms)
↳31 YES
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U4_ga(T27, T28, T29, ap2C_in_ga(T28, X27))
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
U4_ga(T27, T28, T29, ap2C_out_ga(T28, X27)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U5_ga(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_ga(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(cons(T45, T46), cons(T47, T48)) → U7_ga(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U7_ga(T45, T46, T47, T48, ap1A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(cons(T45, T46), cons(T47, T48))
permE_in_ga(cons(T45, T46), cons(T47, T55)) → U8_ga(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
U9_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U4_ga(T27, T28, T29, ap2C_in_ga(T28, X27))
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
U4_ga(T27, T28, T29, ap2C_out_ga(T28, X27)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U5_ga(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_ga(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(cons(T45, T46), cons(T47, T48)) → U7_ga(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U7_ga(T45, T46, T47, T48, ap1A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(cons(T45, T46), cons(T47, T48))
permE_in_ga(cons(T45, T46), cons(T47, T55)) → U8_ga(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
U9_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → U4_GA(T27, T28, T29, ap2C_in_ga(T28, X27))
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → AP2C_IN_GA(T28, X27)
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → U5_GA(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_GA(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_GA(T27, T28, T29, permE_in_ga(T31, T29))
U5_GA(T27, T28, T29, ap2C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(cons(T45, T46), cons(T47, T48)) → U7_GA(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
PERME_IN_GA(cons(T45, T46), cons(T47, T48)) → AP1A_IN_AAAG(X68, T47, X69, T46)
AP1A_IN_AAAG(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_AAAG(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
AP1A_IN_AAAG(cons(T77, X107), T79, X108, cons(T77, T78)) → AP1A_IN_AAAG(X107, T79, X108, T78)
PERME_IN_GA(cons(T45, T46), cons(T47, T55)) → U8_GA(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_GA(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → AP2D_IN_GGGA(T45, T53, T54, X27)
AP2D_IN_GGGA(T93, T94, T95, cons(T93, X134)) → U3_GGGA(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
AP2D_IN_GGGA(T93, T94, T95, cons(T93, X134)) → AP2B_IN_GGA(T94, T95, X134)
AP2B_IN_GGA(cons(T109, T110), T111, cons(T109, X156)) → U2_GGA(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
AP2B_IN_GGA(cons(T109, T110), T111, cons(T109, X156)) → AP2B_IN_GGA(T110, T111, X156)
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_GA(T45, T46, T47, T55, permE_in_ga(T84, T55))
U10_GA(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U4_ga(T27, T28, T29, ap2C_in_ga(T28, X27))
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
U4_ga(T27, T28, T29, ap2C_out_ga(T28, X27)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U5_ga(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_ga(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(cons(T45, T46), cons(T47, T48)) → U7_ga(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U7_ga(T45, T46, T47, T48, ap1A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(cons(T45, T46), cons(T47, T48))
permE_in_ga(cons(T45, T46), cons(T47, T55)) → U8_ga(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
U9_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → U4_GA(T27, T28, T29, ap2C_in_ga(T28, X27))
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → AP2C_IN_GA(T28, X27)
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → U5_GA(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_GA(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_GA(T27, T28, T29, permE_in_ga(T31, T29))
U5_GA(T27, T28, T29, ap2C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(cons(T45, T46), cons(T47, T48)) → U7_GA(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
PERME_IN_GA(cons(T45, T46), cons(T47, T48)) → AP1A_IN_AAAG(X68, T47, X69, T46)
AP1A_IN_AAAG(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_AAAG(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
AP1A_IN_AAAG(cons(T77, X107), T79, X108, cons(T77, T78)) → AP1A_IN_AAAG(X107, T79, X108, T78)
PERME_IN_GA(cons(T45, T46), cons(T47, T55)) → U8_GA(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_GA(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → AP2D_IN_GGGA(T45, T53, T54, X27)
AP2D_IN_GGGA(T93, T94, T95, cons(T93, X134)) → U3_GGGA(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
AP2D_IN_GGGA(T93, T94, T95, cons(T93, X134)) → AP2B_IN_GGA(T94, T95, X134)
AP2B_IN_GGA(cons(T109, T110), T111, cons(T109, X156)) → U2_GGA(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
AP2B_IN_GGA(cons(T109, T110), T111, cons(T109, X156)) → AP2B_IN_GGA(T110, T111, X156)
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_GA(T45, T46, T47, T55, permE_in_ga(T84, T55))
U10_GA(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U4_ga(T27, T28, T29, ap2C_in_ga(T28, X27))
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
U4_ga(T27, T28, T29, ap2C_out_ga(T28, X27)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U5_ga(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_ga(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(cons(T45, T46), cons(T47, T48)) → U7_ga(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U7_ga(T45, T46, T47, T48, ap1A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(cons(T45, T46), cons(T47, T48))
permE_in_ga(cons(T45, T46), cons(T47, T55)) → U8_ga(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
U9_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
AP2B_IN_GGA(cons(T109, T110), T111, cons(T109, X156)) → AP2B_IN_GGA(T110, T111, X156)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U4_ga(T27, T28, T29, ap2C_in_ga(T28, X27))
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
U4_ga(T27, T28, T29, ap2C_out_ga(T28, X27)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U5_ga(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_ga(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(cons(T45, T46), cons(T47, T48)) → U7_ga(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U7_ga(T45, T46, T47, T48, ap1A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(cons(T45, T46), cons(T47, T48))
permE_in_ga(cons(T45, T46), cons(T47, T55)) → U8_ga(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
U9_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
AP2B_IN_GGA(cons(T109, T110), T111, cons(T109, X156)) → AP2B_IN_GGA(T110, T111, X156)
AP2B_IN_GGA(cons(T109, T110), T111) → AP2B_IN_GGA(T110, T111)
From the DPs we obtained the following set of size-change graphs:
AP1A_IN_AAAG(cons(T77, X107), T79, X108, cons(T77, T78)) → AP1A_IN_AAAG(X107, T79, X108, T78)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U4_ga(T27, T28, T29, ap2C_in_ga(T28, X27))
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
U4_ga(T27, T28, T29, ap2C_out_ga(T28, X27)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U5_ga(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_ga(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(cons(T45, T46), cons(T47, T48)) → U7_ga(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U7_ga(T45, T46, T47, T48, ap1A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(cons(T45, T46), cons(T47, T48))
permE_in_ga(cons(T45, T46), cons(T47, T55)) → U8_ga(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
U9_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
AP1A_IN_AAAG(cons(T77, X107), T79, X108, cons(T77, T78)) → AP1A_IN_AAAG(X107, T79, X108, T78)
AP1A_IN_AAAG(cons(T77, T78)) → AP1A_IN_AAAG(T78)
From the DPs we obtained the following set of size-change graphs:
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → U5_GA(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_GA(T27, T28, T29, ap2C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(cons(T45, T46), cons(T47, T55)) → U8_GA(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U4_ga(T27, T28, T29, ap2C_in_ga(T28, X27))
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
U4_ga(T27, T28, T29, ap2C_out_ga(T28, X27)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
permE_in_ga(cons(T27, T28), cons(T27, T29)) → U5_ga(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_ga(T27, T28, T29, ap2C_out_ga(T28, T31)) → U6_ga(T27, T28, T29, permE_in_ga(T31, T29))
permE_in_ga(cons(T45, T46), cons(T47, T48)) → U7_ga(T45, T46, T47, T48, ap1A_in_aaag(X68, T47, X69, T46))
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U7_ga(T45, T46, T47, T48, ap1A_out_aaag(X68, T47, X69, T46)) → permE_out_ga(cons(T45, T46), cons(T47, T48))
permE_in_ga(cons(T45, T46), cons(T47, T55)) → U8_ga(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U9_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, X27))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
U9_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, X27)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U8_ga(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_ga(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_ga(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → U11_ga(T45, T46, T47, T55, permE_in_ga(T84, T55))
U11_ga(T45, T46, T47, T55, permE_out_ga(T84, T55)) → permE_out_ga(cons(T45, T46), cons(T47, T55))
U6_ga(T27, T28, T29, permE_out_ga(T31, T29)) → permE_out_ga(cons(T27, T28), cons(T27, T29))
PERME_IN_GA(cons(T27, T28), cons(T27, T29)) → U5_GA(T27, T28, T29, ap2C_in_ga(T28, T31))
U5_GA(T27, T28, T29, ap2C_out_ga(T28, T31)) → PERME_IN_GA(T31, T29)
PERME_IN_GA(cons(T45, T46), cons(T47, T55)) → U8_GA(T45, T46, T47, T55, ap1A_in_aaag(T53, T47, T54, T46))
U8_GA(T45, T46, T47, T55, ap1A_out_aaag(T53, T47, T54, T46)) → U10_GA(T45, T46, T47, T55, ap2D_in_ggga(T45, T53, T54, T84))
U10_GA(T45, T46, T47, T55, ap2D_out_ggga(T45, T53, T54, T84)) → PERME_IN_GA(T84, T55)
ap2C_in_ga(T37, T37) → ap2C_out_ga(T37, T37)
ap1A_in_aaag(nil, T68, T69, cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69, cons(T68, T69))
ap1A_in_aaag(cons(T77, X107), T79, X108, cons(T77, T78)) → U1_aaag(T77, X107, T79, X108, T78, ap1A_in_aaag(X107, T79, X108, T78))
ap2D_in_ggga(T93, T94, T95, cons(T93, X134)) → U3_ggga(T93, T94, T95, X134, ap2B_in_gga(T94, T95, X134))
U1_aaag(T77, X107, T79, X108, T78, ap1A_out_aaag(X107, T79, X108, T78)) → ap1A_out_aaag(cons(T77, X107), T79, X108, cons(T77, T78))
U3_ggga(T93, T94, T95, X134, ap2B_out_gga(T94, T95, X134)) → ap2D_out_ggga(T93, T94, T95, cons(T93, X134))
ap2B_in_gga(nil, T102, T102) → ap2B_out_gga(nil, T102, T102)
ap2B_in_gga(cons(T109, T110), T111, cons(T109, X156)) → U2_gga(T109, T110, T111, X156, ap2B_in_gga(T110, T111, X156))
U2_gga(T109, T110, T111, X156, ap2B_out_gga(T110, T111, X156)) → ap2B_out_gga(cons(T109, T110), T111, cons(T109, X156))
PERME_IN_GA(cons(T27, T28)) → U5_GA(ap2C_in_ga(T28))
U5_GA(ap2C_out_ga(T31)) → PERME_IN_GA(T31)
PERME_IN_GA(cons(T45, T46)) → U8_GA(T45, ap1A_in_aaag(T46))
U8_GA(T45, ap1A_out_aaag(T53, T47, T54)) → U10_GA(ap2D_in_ggga(T45, T53, T54))
U10_GA(ap2D_out_ggga(T84)) → PERME_IN_GA(T84)
ap2C_in_ga(T37) → ap2C_out_ga(T37)
ap1A_in_aaag(cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69)
ap1A_in_aaag(cons(T77, T78)) → U1_aaag(T77, ap1A_in_aaag(T78))
ap2D_in_ggga(T93, T94, T95) → U3_ggga(T93, ap2B_in_gga(T94, T95))
U1_aaag(T77, ap1A_out_aaag(X107, T79, X108)) → ap1A_out_aaag(cons(T77, X107), T79, X108)
U3_ggga(T93, ap2B_out_gga(X134)) → ap2D_out_ggga(cons(T93, X134))
ap2B_in_gga(nil, T102) → ap2B_out_gga(T102)
ap2B_in_gga(cons(T109, T110), T111) → U2_gga(T109, ap2B_in_gga(T110, T111))
U2_gga(T109, ap2B_out_gga(X156)) → ap2B_out_gga(cons(T109, X156))
ap2C_in_ga(x0)
ap1A_in_aaag(x0)
ap2D_in_ggga(x0, x1, x2)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
ap2B_in_gga(x0, x1)
U2_gga(x0, x1)
PERME_IN_GA(cons(T27, T28)) → U5_GA(ap2C_in_ga(T28))
U5_GA(ap2C_out_ga(T31)) → PERME_IN_GA(T31)
PERME_IN_GA(cons(T45, T46)) → U8_GA(T45, ap1A_in_aaag(T46))
U8_GA(T45, ap1A_out_aaag(T53, T47, T54)) → U10_GA(ap2D_in_ggga(T45, T53, T54))
U10_GA(ap2D_out_ggga(T84)) → PERME_IN_GA(T84)
ap2C_in_ga(T37) → ap2C_out_ga(T37)
ap1A_in_aaag(cons(T68, T69)) → ap1A_out_aaag(nil, T68, T69)
ap1A_in_aaag(cons(T77, T78)) → U1_aaag(T77, ap1A_in_aaag(T78))
ap2D_in_ggga(T93, T94, T95) → U3_ggga(T93, ap2B_in_gga(T94, T95))
U1_aaag(T77, ap1A_out_aaag(X107, T79, X108)) → ap1A_out_aaag(cons(T77, X107), T79, X108)
U3_ggga(T93, ap2B_out_gga(X134)) → ap2D_out_ggga(cons(T93, X134))
ap2B_in_gga(nil, T102) → ap2B_out_gga(T102)
ap2B_in_gga(cons(T109, T110), T111) → U2_gga(T109, ap2B_in_gga(T110, T111))
U2_gga(T109, ap2B_out_gga(X156)) → ap2B_out_gga(cons(T109, X156))
U10GA1 > ap2Dinggga3 > ap1Ainaaag1 > ap2Coutga1 > cons2 > U5GA1 > PERMEINGA1 > U1aaag2 > U8GA2 > ap2Bingga2 > U2gga2 > U3ggga2 > ap2Doutggga1 > ap2Boutgga1 > nil > ap1Aoutaaag3 > ap2Cinga1
nil=4
ap2C_in_ga_1=3
ap2C_out_ga_1=2
ap1A_in_aaag_1=3
ap2B_out_gga_1=4
ap2D_out_ggga_1=3
PERME_IN_GA_1=3
U5_GA_1=1
U10_GA_1=1
cons_2=1
ap1A_out_aaag_3=0
U1_aaag_2=1
ap2D_in_ggga_3=0
U3_ggga_2=0
ap2B_in_gga_2=0
U2_gga_2=1
U8_GA_2=1
ap2C_in_ga(x0)
ap1A_in_aaag(x0)
ap2D_in_ggga(x0, x1, x2)
U1_aaag(x0, x1)
U3_ggga(x0, x1)
ap2B_in_gga(x0, x1)
U2_gga(x0, x1)